(declare-fun x () String)
(declare-fun i () Int)
(assert (distinct (str.at x i) "b"))
(assert (xor (>= i 215) (>= i (str.len x))))
(assert (>= (str.len x) 216))
(check-sat)
(declare-fun x () String)
(declare-fun i () Int)
(assert (distinct (str.at x i) "b"))
(assert (xor (>= i 215) (>= i (str.len x))))
(assert (>= (str.len x) 216))
(check-sat)
